WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2,eval#1,main,sub#2} and constructors {Add,Nat,Sub
            ,Succ,Zero}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          add#2#(Zero(),x8) -> c_2()
          eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          eval#1#(Nat(x1)) -> c_4()
          eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          main#(x12) -> c_6(eval#1#(x12))
          sub#2#(x8,Zero()) -> c_7()
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
          sub#2#(Zero(),Succ(x16)) -> c_9()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            add#2#(Zero(),x8) -> c_2()
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Nat(x1)) -> c_4()
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(x8,Zero()) -> c_7()
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
            sub#2#(Zero(),Succ(x16)) -> c_9()
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,7,9}
        by application of
          Pre({2,4,7,9}) = {1,3,5,6,8}.
        Here rules are labelled as follows:
          1: add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          2: add#2#(Zero(),x8) -> c_2()
          3: eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          4: eval#1#(Nat(x1)) -> c_4()
          5: eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          6: main#(x12) -> c_6(eval#1#(x12))
          7: sub#2#(x8,Zero()) -> c_7()
          8: sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
          9: sub#2#(Zero(),Succ(x16)) -> c_9()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak DPs:
            add#2#(Zero(),x8) -> c_2()
            eval#1#(Nat(x1)) -> c_4()
            sub#2#(x8,Zero()) -> c_7()
            sub#2#(Zero(),Succ(x16)) -> c_9()
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
             -->_1 add#2#(Zero(),x8) -> c_2():6
             -->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
          
          2:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_3 eval#1#(Nat(x1)) -> c_4():7
             -->_2 eval#1#(Nat(x1)) -> c_4():7
             -->_1 add#2#(Zero(),x8) -> c_2():6
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
          
          3:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
             -->_1 sub#2#(Zero(),Succ(x16)) -> c_9():9
             -->_1 sub#2#(x8,Zero()) -> c_7():8
             -->_3 eval#1#(Nat(x1)) -> c_4():7
             -->_2 eval#1#(Nat(x1)) -> c_4():7
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
          
          4:S:main#(x12) -> c_6(eval#1#(x12))
             -->_1 eval#1#(Nat(x1)) -> c_4():7
             -->_1 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_1 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
          
          5:S:sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
             -->_1 sub#2#(Zero(),Succ(x16)) -> c_9():9
             -->_1 sub#2#(x8,Zero()) -> c_7():8
             -->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
          
          6:W:add#2#(Zero(),x8) -> c_2()
             
          
          7:W:eval#1#(Nat(x1)) -> c_4()
             
          
          8:W:sub#2#(x8,Zero()) -> c_7()
             
          
          9:W:sub#2#(Zero(),Succ(x16)) -> c_9()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: eval#1#(Nat(x1)) -> c_4()
          8: sub#2#(x8,Zero()) -> c_7()
          9: sub#2#(Zero(),Succ(x16)) -> c_9()
          6: add#2#(Zero(),x8) -> c_2()
* Step 4: RemoveHeads WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
           -->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
        
        2:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
           -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
           -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
           -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
           -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
           -->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
        
        3:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
           -->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
           -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
           -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
           -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
           -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
        
        4:S:main#(x12) -> c_6(eval#1#(x12))
           -->_1 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
           -->_1 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
        
        5:S:sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
           -->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(4,main#(x12) -> c_6(eval#1#(x12)))]
* Step 5: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
          add#2(Zero(),x8) -> x8
          eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
          eval#1(Nat(x1)) -> x1
          eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
          sub#2(x8,Zero()) -> x8
          sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
          sub#2(Zero(),Succ(x16)) -> Zero()
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
* Step 6: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
        and a lower component
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        Further, following extension rules are added to the lower component.
          eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
          eval#1#(Add(x2,x1)) -> eval#1#(x1)
          eval#1#(Add(x2,x1)) -> eval#1#(x2)
          eval#1#(Sub(x2,x1)) -> eval#1#(x1)
          eval#1#(Sub(x2,x1)) -> eval#1#(x2)
          eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
          
          2:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
** Step 6.a:3: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          Add :: ["A"(14) x "A"(14)] -(14)-> "A"(14)
          Sub :: ["A"(14) x "A"(14)] -(14)-> "A"(14)
          eval#1# :: ["A"(14)] -(5)-> "A"(1)
          c_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
          c_5 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "Sub_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "c_5_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
        2. Weak:
          eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
** Step 6.a:4: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
        - Weak DPs:
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          Add :: ["A"(11) x "A"(11)] -(11)-> "A"(11)
          Sub :: ["A"(11) x "A"(11)] -(11)-> "A"(11)
          eval#1# :: ["A"(11)] -(5)-> "A"(0)
          c_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          c_5 :: ["A"(0) x "A"(0)] -(0)-> "A"(14)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "Sub_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "c_5_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
        2. Weak:
          

** Step 6.b:1: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak DPs:
            eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
            eval#1#(Add(x2,x1)) -> eval#1#(x1)
            eval#1#(Add(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> eval#1#(x1)
            eval#1#(Sub(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          Add :: ["A"(6) x "A"(6)] -(0)-> "A"(6)
          Add :: ["A"(8) x "A"(8)] -(0)-> "A"(8)
          Nat :: ["A"(6)] -(6)-> "A"(6)
          Sub :: ["A"(6) x "A"(6)] -(0)-> "A"(6)
          Sub :: ["A"(8) x "A"(8)] -(0)-> "A"(8)
          Succ :: ["A"(4)] -(4)-> "A"(4)
          Succ :: ["A"(5)] -(5)-> "A"(5)
          Succ :: ["A"(1)] -(1)-> "A"(1)
          Zero :: [] -(0)-> "A"(5)
          Zero :: [] -(0)-> "A"(1)
          Zero :: [] -(0)-> "A"(15)
          add#2 :: ["A"(5) x "A"(5)] -(0)-> "A"(5)
          eval#1 :: ["A"(6)] -(0)-> "A"(5)
          sub#2 :: ["A"(5) x "A"(1)] -(0)-> "A"(5)
          add#2# :: ["A"(4) x "A"(0)] -(6)-> "A"(0)
          eval#1# :: ["A"(8)] -(14)-> "A"(0)
          sub#2# :: ["A"(4) x "A"(5)] -(7)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(0)
          c_8 :: ["A"(0)] -(0)-> "A"(14)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "Add_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
          "Nat_A" :: ["A"(1)] -(1)-> "A"(1)
          "Sub_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
          "Succ_A" :: ["A"(1)] -(1)-> "A"(1)
          "Zero_A" :: [] -(0)-> "A"(1)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_8_A" :: ["A"(0)] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
        2. Weak:
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
** Step 6.b:2: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
            eval#1#(Add(x2,x1)) -> eval#1#(x1)
            eval#1#(Add(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> eval#1#(x1)
            eval#1#(Sub(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
            ,Sub,Succ,Zero}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          Add :: ["A"(4) x "A"(4)] -(4)-> "A"(4)
          Nat :: ["A"(4)] -(0)-> "A"(4)
          Sub :: ["A"(4) x "A"(4)] -(0)-> "A"(4)
          Succ :: ["A"(1)] -(1)-> "A"(1)
          Succ :: ["A"(0)] -(0)-> "A"(0)
          Zero :: [] -(0)-> "A"(1)
          Zero :: [] -(0)-> "A"(0)
          Zero :: [] -(0)-> "A"(14)
          add#2 :: ["A"(1) x "A"(1)] -(3)-> "A"(1)
          eval#1 :: ["A"(4)] -(0)-> "A"(1)
          sub#2 :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
          add#2# :: ["A"(1) x "A"(0)] -(7)-> "A"(0)
          eval#1# :: ["A"(4)] -(11)-> "A"(0)
          sub#2# :: ["A"(1) x "A"(0)] -(1)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(14)
          c_8 :: ["A"(0)] -(0)-> "A"(14)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "Nat_A" :: ["A"(1)] -(0)-> "A"(1)
          "Sub_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
          "Succ_A" :: ["A"(1)] -(1)-> "A"(1)
          "Zero_A" :: [] -(0)-> "A"(1)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_8_A" :: ["A"(0)] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        2. Weak:
          

WORST_CASE(?,O(n^2))